Conversation
89605eb to
76ec439
Compare
…relation verification
…ion for non native msm
907433f to
73d8275
Compare
|
/claude-review |
Code ReviewSummaryThis PR implements MSM (Multi-Scalar Multiplication) as a black-box opcode in the R1CS compiler, dispatching Noir's ReviewCorrectness & Soundness The overall proof strategy is sound. Phases 2 + 3 jointly prove
One soundness concern to flag:
Code Quality Blocking:
Minor: Missing Non-blocking: Non-blocking: No comment on Grumpkin hardcode. In Testing
Suggestions (non-blocking)
Verdict🔄 Request changes — The |
| // --------------------------------------------------------------------------- | ||
|
|
||
| /// Shared core for `add_mod_p_multi` and `sub_mod_p_multi`. | ||
| fn add_sub_mod_p_core( |
There was a problem hiding this comment.
In add_sub_mod_p_core, negate_mod_p_multi, and less_than_p_check_multi, each limb iteration emits two linear constraints: one for the intermediate sum (v_offset/v/v_diff) and one for the remainder (r[i]/ri/d_i). These can be merged into a single constraint per limb.
For example in add_sub_mod_p_core, currently:
C1: (a[i] + b[i] + offset - p[i]*q + carry_prev) * 1 = v_offset
C2: (v_offset - carry * 2^W) * 1 = r[i]
Can become:
CM: (a[i] + b[i] + offset - p[i]*q + carry_prev - carry * 2^W) * 1 = r[i]
| /// SafeInverse outputs 0 when the input is 0, and is solved in the Other | ||
| /// layer (not batch-inverted), so zero inputs don't poison the batch. | ||
| #[must_use] | ||
| pub fn compute_is_zero(compiler: &mut NoirToR1CSCompiler, value: usize) -> usize { |
There was a problem hiding this comment.
nit: compute_is_zero allocates a value_mul_value_inv witness that never appears in any constraint, it's only used to compute is_zero via the Sum builder. Could be eliminated with a direct WitnessBuilder::IsZero which can be created explicitly
There was a problem hiding this comment.
it is called once per msm point and change will add another variant tot witness builder for like 2-3 witness count. Do you think we should go for this change ?
|
|
||
| for pt in merged_points { | ||
| let offset = EcPoint { | ||
| x: ops.constant_limbs(offset_x_values), |
There was a problem hiding this comment.
constant_limbs(offset_x_values) and constant_limbs(offset_y_values) are called inside the per-point loop, allocating fresh pinned witnesses and constraints each iteration for identical values. Limbs is Copy, so these can be hoisted before the loop and reused. Same applies to the duplicate offset_x allocations in accumulate_and_constrain_outputs
There was a problem hiding this comment.
after guassian elimination idts it should matter but I have added this change because it looks clean and the right way to add constants
| y: { | ||
| let neg_off_y = ops.constant_limbs(&neg_offset_y_values); | ||
| let neg_g_y = ops.constant_limbs(&neg_gen_y_values); | ||
| ops.select(all_skipped, neg_off_y, neg_g_y) |
There was a problem hiding this comment.
all_skipped is already boolean-constrained by the ops.select at line 395. The second ops.select adds a duplicate flag * flag = flag constraint (via constrain_flag inside select). Could use select_unchecked here instead.
# Conflicts: # Cargo.lock # provekit/prover/src/lib.rs
|
Avoid use of .unwrap(), either use .expect("") or float the error with Result. |
MSM Black Box Support
curve arithmetic over multi-limb field elements.
following the same pattern as SHA256 spread optimization.
half-GCD and interleaved two-point windowed scalar multiplication.
modular inverse) used in witness solving.
Performance Comparison :
This is for 2 points call for msm: s_1[p_1] * s_2[p_2]